package no.uio.ifi.cop.prover;

import java.util.Stack;


import no.uio.ifi.cop.cl.Axiom;
import no.uio.ifi.cop.cl.Conjunction;
import no.uio.ifi.cop.cl.Predicate;
import no.uio.ifi.cop.cl.Substitution;
import no.uio.ifi.cop.util.Tuple;

/**
 * This interface defines the needed functionality
 * for a class to be used by the Prover.
 *
 *
 * @version 1.0
 * @author  bjarneh@ifi.uio.no
 */


public interface RuleFinder{
    /**
     * Add a new axiom from a geometric theory.
     *
     * @param ax is an axiom in a geometric theory
     */
    public void addRule(Axiom ax);

    /**
     * Get a matching rule and its substitution.
     *
     *
     * @return Tuple<Axiom,Substitution> holds a matching
     * rule (axiom) and the substitution used to get match.
     * Returns null if no match is present.
     */
    public Tuple<Axiom, Substitution> getNextMatch();

    /**
     * Add a new fact, to be matched against rules/axioms.
     *
     * @param p is a fact which should be matched against
     * rules (axioms) in geometric theory.
     */
    public void addPredicate(Predicate p);

    /**
     * Boolean test on whether there are more 
     * matching substitutions.
     * 
     * @return true if no more matches can be found,
     * false otherwise.
     */
    public boolean exhausted();

    /**
     * Return a non-shallow copy of RuleFinder.
     *
     * @return a copy of yourself, a shallow clone will
     * not do in most cases since branches don't share
     * fact-sets.
     */
    public RuleFinder clone();

    /**
     * Stop execution of this thread.
     */
    public void stop();
}
